Nuprl Lemma : interface-link_wf
11,40
postcript
pdf
A
,
B
:(Id
MsgA),
l
:IdLnk,
tg
:Id. interface-link(
A
;
B
;
l
;
tg
)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
,
interface-link(
A
;
B
;
l
;
tg
)
,
P
&
Q
Lemmas
ma-declm
wf
,
lsrc
wf
,
ldst
wf
,
not
wf
,
Id
wf
,
IdLnk
wf
,
msga
wf
origin
A, B:(Id
MsgA), l:IdLnk, tg:Id. interface-link(A;B;l;tg) 
A, B:(IdMsgA), l:IdLnk, tg:Id. interface-link(A;B;l;tg) x:A. B(x) T